pre-init1-p(es;i;x;X;x0;a;T;P)
== ((v:T. P(x0,v))  (e:E. loc(e) = i))
== & vartype(i;x)  X
== & e@i. kind(e) = locl(a)  valtype(e)  T & P((x when e),val(e))
== & & e@i. ee'.kind(e') = locl(a)  (v:T. P((x after e'),v))
== & @i x initially x0:X 

latex

---

clarification:

pre-init1-p(es;i;x;X;x0;a;T;P)
== ((v:T. P(x0,v))  (e:es-E(es). es-loc(es; e) = i  Id))
== & es-vartype(es; i; x)  X
== & alle-at(es;i;e.es-kind(es; e) = locl(a)  Knd
== & alle-at(es;i;e. es-valtype(es; e)  T & P(es-when(es; x; e),es-val(es; e)))
== & & alle-at(es;i;e.existse-ge(es;e;e'.es-kind(es; e') = locl(a)  Knd
== & &  (v:T. P(es-after(es; x; e'),v))))
== & init-p(es; i; X; x; x0) 

latex

Definitions	x:A. B(x), E, Id, loc(e), vartype(i;x), P & Q, P  Q, A & B, valtype(e), x when e, val(e), e@i. P(e), ee'.P(e'), P  Q, s = t, Knd, kind(e), locl(a), x:A. B(x), A, f(a), (x after e), @i x initially v:T
FDL editor aliases	pre-init1-p